Nuprl Lemma : atom2-deq-aux
11,40
postcript
pdf
a
,
b
:atom{2:n}. (
a
=
b
)
(
eq_atom{2:n}(
a
;
b
))
latex
Definitions
x
:
A
B
(
x
)
,
P
Q
,
P
Q
,
prop{i:l}
,
Type
,
s
=
t
,
atom{$n:n}
,
b
,
eq_atom{$n:n}(
x
;
y
)
,
x
:
A
.
B
(
x
)
,
t
T
,
P
Q
,
P
Q
Lemmas
eq
atom
wf2
,
assert
wf
,
assert
of
eq
atom2
origin
a,b:atom{2:n}. (a = b) 
(
eq_atom{2:n}(a; b)) a,b:atom{2:n}. (a = b) (eq_atom{2:n}(a; b)) 
B(x) Q
Qbx:A. B(x)
T Q Q